Inference at * 
Iof proof for Lemma fseg select:


  T:Type, l1, l2:(T List).
  fseg(T;l1;l2)
   ((||l1||  ||l2||) c (i:. (i < ||l1||)  (l1[i] = l2[((||l2|| - ||l1||)+i)]))) 

latex

 by ((Auto') 
CollapseTHEN ((Try (((BLemma `fseg_length`) 
CollapseTHEN (Auto)))))) 

latex

C1: 

C1: 1. T : Type
C1: 2. l1 : T List
C1: 3. l2 : T List
C1: 4. fseg(T;l1;l2)
C1: 5. i : 
C1: 6. i < ||l1||
C1:   l1[i] = l2[((||l2|| - ||l1||)+i)]
C2: 

C2: 1. T : Type
C2: 2. l1 : T List
C2: 3. l2 : T List
C2: 4. (||l1||  ||l2||) c (i:. (i < ||l1||)  (l1[i] = l2[((||l2|| - ||l1||)+i)]))
C2:   fseg(T;l1;l2)
C.

Definitions	P  Q, P & Q, P  Q, i  j , x:A  B(x), A c B, , S  T, |g|, , {x:A| B(x)} , l[i], #$n, n+m, n - m, ||as||, , a < b, type List, t  T, Type, s = t, x:A. B(x), P  Q, x:AB(x), A  B, fseg(T;L1;L2)
Lemmas	fseg wf, le wf, length wf1, nat wf, select wf, fseg length